ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), L:event-info(ds;da) List.
ecl-halt(ds;da;x)(0,L)  isl(ecl-halt-kind(x))  1of(last(L)) = outl(ecl-halt-kind(x))  Knd 

latex

Definitions

b, Void, x:AB(x), P  Q, False, A, x:A. B(x), event-info(ds;da), l[i], 1of(t), <a,b>, Knd, s = t, last(L), hd(l), i<j, ij, t  T, x:A. B(x), Top, type List, S  T, State(ds), Valtype(da;k), x:AB(x), nil, car.cdr, null(as), as @ bs, ecl-halt-kind(x), Unit, Type, outl(x), Prop, {x:A| B(x) }, x.A(x), x. t(x), P & Q, x:A. B(x), Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, {T}, SQType(T), s ~ t, left+right, f(a), A & B, let x,y,z = a in t(x;y;z), True, ecl-halt(ds;da;x), AB, , , P  Q, #$n, a<b, P  Q, inr(x), inl(x), f(x)?z, ecl(ds;da), isl(x), (xL.P(x)), (x  l), star-append(T;P;Q), l1  l2, , xL. P(x), ecl ind eclcatch compseq tag def, ecl ind eclthrow compseq tag def, ecl ind eclact compseq tag def, ecl ind eclrepeat compseq tag def, ecl ind eclor compseq tag def, ecl ind ecland compseq tag def, ecl ind eclseq compseq tag def, ecl ind eclbase compseq tag def, a:A fp B(a), Id

Lemmas

Id wf, fpf wf, ecl-induction, true wf, l all wf, bool wf, iseg wf, star-append wf, l member wf, l exists wf, ecl-halt wf, isl wf, nat wf, ecl wf, ecl-halt-nil, le wf, Knd sq, pi1 wf, outl wf, unit wf, ecl-halt-kind wf, append wf, Knd wf, decl-state wf, ma-valtype wf, last wf, not wf, assert wf, null wf3, false wf, last append, top wf, event-info wf